package com.googlecode.kipler.container.dl;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import com.googlecode.kipler.common.Copyable;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.concept.ConceptName;
import com.googlecode.kipler.syntax.formula.ConceptDefinition;
import com.googlecode.kipler.syntax.formula.Formula;
import com.googlecode.kipler.syntax.formula.ConceptDefinition.Type;
import com.googlecode.kipler.transformations.UnfoldingVisitor;
import com.googlecode.kipler.transformations.UsedConceptNameVisitor;

/**
 * 
 * @author İnanç Seylan
 * 
 */
public class UnfoldableTBox implements Copyable<UnfoldableTBox>, FormulaBase {

	private Map<ConceptName, ConceptDefinition> conceptDefs = new HashMap<ConceptName, ConceptDefinition>();

	private boolean isUnfoldableWith(ConceptDefinition cd) {
		return !isTopOrBottomAtSides(cd) && !cd.isNegated() && !isGCI(cd)
				&& !destroysUniqueness(cd) && isAcyclicWith(cd);
	}

	private boolean isTopOrBottomAtSides(ConceptDefinition cd) {
		return cd.getLhs().equals(ConceptName.topConcept())
				|| cd.getRhs().equals(ConceptName.topConcept())
				|| cd.getLhs().equals(ConceptName.bottomConcept())
				|| cd.getRhs().equals(ConceptName.bottomConcept());
	}

	private boolean isGCI(ConceptDefinition cd) {
		return !(cd.getLhs() instanceof ConceptName) || cd.getLhs().isNegated();
	}

	private boolean destroysUniqueness(ConceptDefinition cd) {
		return conceptDefs.containsKey(cd.getLhs());
	}

	private boolean isAcyclicWith(ConceptDefinition conDef) {
		UsedConceptNameVisitor visitor = new UsedConceptNameVisitor(this);
		conDef.getRhs().accept(visitor);
		return !visitor.getUsedConcepts().contains(conDef.getLhs());
	}

	public void add(Formula formula) throws UnsatisfiableException {
		if (formula instanceof ConceptDefinition) {
			add((ConceptDefinition) formula);
		}
	}

	public boolean add(ConceptDefinition conDef) {
		boolean result = false;
		if (isUnfoldableWith(conDef)) {
			conceptDefs.put((ConceptName) conDef.getLhs(), conDef);
			result = true;
		}
		return result;
	}

	public ConceptDefinition getDefinition(ConceptName c) {
		ConceptDefinition result = null;
		if (conceptDefs.containsKey(c)) {
			result = conceptDefs.get(c);
		}
		return result;
	}

	public Concept unfold(ConceptName c) {
		Concept result = null;
		if (containsCompletely(c)) {
			UnfoldingVisitor visitor = new UnfoldingVisitor(this);
			c.accept(visitor);
			result = visitor.getResult();
		}
		return result;
	}

	public Concept getDescription(ConceptName c) {
		Concept result = null;
		boolean isNegationAsked = c.isNegated();
		ConceptName posC = isNegationAsked ? c.copy().toggleNegated() : c;
		if (!isNegationAsked && conceptDefs.containsKey(posC)) {
			result = conceptDefs.get(posC).getRhs();
		} else if (isNegationAsked && conceptDefs.containsKey(posC)) {
			ConceptDefinition conDef = conceptDefs.get(posC);
			if (conDef.getType() == Type.NON_PRIMITIVE) {
				result = conDef.getRhs().copy().toggleNegated();
			}
		}
		return result;
	}

	private boolean containsCompletely(ConceptName c) {
		boolean isNegationAsked = c.isNegated();
		ConceptName posC = isNegationAsked ? c.copy().toggleNegated() : c;
		return conceptDefs.containsKey(posC);
	}

	public boolean contains(Formula formula) {
		boolean result = false;
		if (formula instanceof ConceptDefinition) {
			result = contains((ConceptDefinition) formula);
		}
		return result;
	}

	public boolean contains(ConceptDefinition cd) {
		boolean result = false;
		if (!cd.isNegated() && cd.getLhs() instanceof ConceptName) {
			ConceptName c = (ConceptName) cd.getLhs();
			if (conceptDefs.containsKey(c)) {
				result = conceptDefs.get(c).equals(cd);
			}
		}
		return result;
	}

	public UnfoldableTBox copy() {
		UnfoldableTBox tbox = new UnfoldableTBox();
		tbox.conceptDefs = new HashMap<ConceptName, ConceptDefinition>(
				conceptDefs);
		return tbox;
	}

	@Override
	public boolean equals(Object obj) {
		if (obj != null && (obj.getClass().equals(this.getClass()))) {
			UnfoldableTBox other = (UnfoldableTBox) obj;
			return conceptDefs.equals(other.conceptDefs);
		}
		return false;
	}

	@Override
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		for (Formula f : getFormulas())
			buffer.append(f + ", ");
		buffer.delete(buffer.length() - 2, buffer.length());
		return buffer.toString();
	}

	public Set<Formula> getFormulas() {
		return new HashSet<Formula>(conceptDefs.values());
	}

	public boolean isSatisfiable() {
		return true;
	}

	public int size() {
		return conceptDefs.size();
	}

}
